Skip to content

feat(GRewrite): new grw implementation#38318

Draft
JovanGerb wants to merge 37 commits intoleanprover-community:masterfrom
JovanGerb:Jovan-grw-2
Draft

feat(GRewrite): new grw implementation#38318
JovanGerb wants to merge 37 commits intoleanprover-community:masterfrom
JovanGerb:Jovan-grw-2

Conversation

@JovanGerb
Copy link
Copy Markdown
Contributor

@JovanGerb JovanGerb commented Apr 20, 2026 •
edited
Loading

This PR adds a new implementation of the grewrite tactic. It has some advantages and disadvantages compared to the current grewrite implementation. Most notably, the new version can rewrite terms with bound variables. For now, this comes at the cost of having to fully elaborate the grewrite argument before doing the rewrite.

The idea is to either

  • replace grw with the new implementation, and add grw' for the old implementation (currently done in this PR)
  • keep grw the same, and add grw' with the new implementation
  • let grw try both implementations, so that it succeeds if one of them does.

Breaking changes:

  • The order of side goals is slightly different.
  • Elaboration of the grw argument works less well.
  • When there are multiple places to rewrite, the new version rewrites everywhere, even if these require different instantiations of the lemma.

Open in Gitpod

@JovanGerb JovanGerb marked this pull request as draft April 20, 2026 22:44
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Apr 20, 2026

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 20, 2026 •
edited
Loading

PR summary f51ea0eb59

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
There are 7247 files with changed transitive imports taking up over 321825 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

Declarations diff

+ GCongrHyp
+ GRewriteLemma
+ GRewriteLemma.apply
+ GRewriteLemma.getValue
+ GRewriteLemma.metaTelescope
+ GRewriteM
+ _root_.Lean.MVarId.applyRflOrId
+ _root_.Lean.MVarId.grewrite'
+ and_mono
+ applyGCongrLemma
+ biSup_inf_le
+ elabGRewrite
+ elabGRewriteLemma
+ evalGRewriteSeq'
+ ge_imp_ge_of_le_of_le
+ getRel'
+ grewriteLocalDecl'
+ grewriteTarget'
+ gt_imp_gt_of_le_of_le
+ imp_mono
+ makeGCongrGoal
- _root_.Lean.MVarId.applyWithArity
- and_right_mono
- imp_right_mono
- imp_trans

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 21, 2026
@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 22, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@JovanGerb